package tr.edu.ege.kipler.satisfiability.completion.rules.formula;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.container.WcsData;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.syntax.KModality;
import tr.edu.ege.kipler.syntax.ModalExpression;
import tr.edu.ege.kipler.syntax.TypedModality;
import tr.edu.ege.kipler.syntax.WorldElement;

/**
 * This method handles a modal formula in which the modal operator is the
 * necessity operator having the axioms of the standard modal logic K.
 * 
 * @author İnanç Seylan
 */
public class BoxFormulaRule extends CompletionRule {

	private boolean applied;

	/**
	 * Since we have many modal operators (therefore necessity and possibility
	 * operators), this rule selects necessitations according to the type of the
	 * necessity operator (belief, intention, etc.) we want. This field
	 * indicates the necessity operator.
	 */
	private TypedModality operator;

	/**
	 * Default constructor that initializes the {@link #operator} field.
	 * 
	 * @param operator
	 *            The operator
	 */
	public BoxFormulaRule(TypedModality operator) {
		this.operator = operator;
	}

	public boolean isApplied() {
		return applied;
	}

	/**
	 * For all necessitations with the specified modal operator, call the
	 * {@link #addNecessiateToAccessibleWorlds(ModalFormula)} method
	 * 
	 * @see tr.edu.ege.seagent.alcbi.satisfiability.frame.CompletionRule#apply()
	 * 
	 * TODO: This method will throw exception if the accessibility relation is
	 * reflexive for a world (ConcurrentModificationException).
	 */
	public void apply() throws UnsatisfiableException {
		applied = false;
		for (WorldElement f : getWorld().getPBox().getFormulas()) {
			if (f instanceof ModalExpression) {
				ModalExpression mf = (ModalExpression) f;
				if (mf.getOperator().isNecessiate()
						&& mf.getOperator() instanceof TypedModality
						&& mf.getOperator() instanceof KModality) {
					TypedModality modality = (TypedModality) mf.getOperator();
					if (modality.getType().equals(operator.getType())) {
						addNecessiateToAccessibleWorlds(mf);
					}
				}
			}
		}
	}

	/**
	 * Adds the necessiate of the given modal formula to all the worlds that are
	 * accessible from this world by the specified modal operator which is
	 * indexed by the agent in the given modal formula.
	 * 
	 * @param mf
	 *            The modal formula whose necessiate will be added to all the
	 *            worlds accessible from this world by the given modal operator
	 *            and agent name.
	 */
	protected void addNecessiateToAccessibleWorlds(ModalExpression mf)
			throws UnsatisfiableException {
		String relation = ((KModality) mf.getOperator()).getRelation();
		for (World world : getWcs().getAccWorldsByFrom(relation, getWorld())) {
			if (!world.contains(mf.getExpression())) {
				WcsData wcsData = getWcs().getData();
				wcsData.getLogger().info(
						"WCS " + getWcs().getId()
								+ " Box formula rule: Adding "
								+ mf.getExpression() + " to the world "
								+ world.getName());
				wcsData.getDependencyManager().move(mf.getExpression(), mf);
				/*
				 * TODO: manage dependency for accessibility relation
				 * wcsData.getDependencyManager().move(mf.getExpression(), ra);
				 */
				world.add(mf.getExpression());
				applied = true;
			}
		}
	}
}
